es:ES, i, x:Id, T, A:Type, f:(TA), Lx:(Knd List).
@i only Lx affect x:T
 e@i. (kind(e)  Lx)  (f((x after e)) = f(x when e)  A)
 e@i. f(x when e) = f(x when es-init(es;e)) 

latex

Definitions	@i only L affect x:T, ES, t  T, Id, Type, x:AB(x), Knd, type List, x:A. B(x), x when e, vartype(i;x), (x after e), loc(e), s = t, E, {x:A| B(x)} , f(a), x(s), , kind(e), (x  l), P  Q, x. t(x), e@i. P(e), x:A  B(x), <a, b>, A c B, left + right, P  Q, Dec(P)
Lemmas	es-vartype wf, decidable l member, decidable equal Kind, es-constant1, alle-at wf, l member wf, es-kind wf, es-E wf, es-loc wf, es-after wf, es-when wf, es-frame wf, Knd wf, Id wf, event system wf